es:ES, i, x:Id, T, A:Type, f:(TA).
vartype(i;x)  T
 e@i. f((x after e)) = f(x when e)
 e@i. f(x when e) = f(x when es-init(es;e)) 

latex

Definitions	t  T, x:A. B(x), E, Type, loc(e), x:AB(x), Id, Prop, vartype(i;x), b, Void, x:AB(x), P  Q, False, A, P  Q, P & Q, P  Q, f(a), <a,b>, e@i. P(e), first(e), left+right, , A & B, x.A(x), ES, {x:A| B(x) }, (x after e), es-init(es;e), x when e, x(s), s = t, x. t(x), s ~ t, {T}, SQType(T), A/x,y. B(x;y), 1of(t), True, T, @i always.P(x)
Lemmas	es-first-unique, es-first-init, squash wf, true wf, not wf, alle-at wf, es-after wf, event system wf, es-invariant1, assert wf, es-first wf, es-when wf, es-init wf, es-loc-init, es-loc-pred, es-vartype wf, Id wf, es-loc wf, es-E wf